$\forall$$l$:IdLnk, ${\it dt}$:fpf(Id; ${\it tg}$.Type). lnk{-}decl($l$; ${\it dt}$) $\in$ fpf(Knd; $k$.Type)